| Definitions | x:A  B(x),  b, ES, Type, IdLnk, Atom$n, Id, a:A fp B(a), x:A B(x),  e@i. P(e), x dom(f). v=f(x)   P(x;v), @i discrete ds, s = t, if b then t else f fi , t T, {T}, P Q, x:A. B(x), SQType(T), loc(e), s ~ t, t.1, E, (e < e'), e c e', Knd, P & Q, A c B, <a, b>,  , discrete state@i, State(ds), (discrete state after e), f(a), left + right,  , Unit, False, True, case b of inl(x) => s(x) | inr(y) => t(y),  A, isrcv(e), sender(e), let x,y = A in B(x;y), e loc e' , (e <loc e'), P  Q, EqDecider(T), EOrderAxioms(E; pred?; info), EState(T), kindcase(k; a.f(a); l,t.g(l;t) ), Msg(M), type List,  ,  , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), e < e', r s, constant_function(f;A;B), Top,  x:A. B(x), rcv(l,tg), kind(e), {x:A| B(x)} ,   x. t(x), locl(a), source(l), P  Q, P Q, val(e), state@i, (state when e), valtype(e), (discrete state when e), x.A(x), f(x), @i(x:T), IdDeq, x dom(f), vartype(i;x), f(x)?z, discrete-weak-precond-send-p(es;T;A;l;tg;a;ds;P;f),  T |
f:({s:State(ds)|